STM: not-false

STM: not-true

STM: simplify-equal-imp

STM: equal-top

STM: subtype-top

STM: decidable implies better

STM: list-subtype

STM: null-ite

STM: typed-null-ite

STM: decidable equal union

STM: decidable equal unit

STM: length-append

STM: filter-commutes

STM: null-map

STM: null wf3

STM: member-zip

STM: decidable equal product

STM: decidable equal nat plus

STM: decidable equal nat

STM: filter wf2

STM: no repeats filter2

STM: filter tt

STM: general-append-cancellation

STM: append-cancellation

STM: append-impossible

STM: append-impossible2

STM: append-cancellation-right

STM: append iseg

STM: iseg append iff

STM: iseg append single

STM: iseg append length

STM: iseg-subtype

STM: list accum append

STM: last induction

STM: last-cons

STM: last append

STM: list accum functionality

STM: list accum filter

STM: compat-iff-common-iseg

ABS: l_contains(T;A;B)

STM: l contains wf

STM: l contains weakening

STM: l contains append

STM: l contains append2

STM: l contains append3

STM: l contains-append4

STM: l contains disjoint

STM: l disjoint append

STM: l disjoint append2

STM: l disjoint-symmetry

STM: l disjoint singleton

ABS: xL.P(x)

STM: l-all wf

STM: l-all-iff

ABS: f[x:=v]

STM: update wf

ABS: l[i:=x]

STM: list update wf

STM: list update select

STM: list update length

STM: iseg antisymmetry

STM: compat-cons

STM: compat-append

STM: compat-append2

STM: compat symmetry

STM: compat-iseg

STM: compat-iseg2

ABS: sorted(L)

STM: sorted wf

STM: sorted-cons

STM: sorted-filter

ABS: s-insert(x;l)

STM: s-insert wf

STM: member-s-insert

STM: s-insert-sorted

STM: s-insert-no-repeats

ABS: s-filter(p;as)

STM: s-filter wf

ABS: merge(as;bs)

STM: merge wf

STM: member-merge

STM: sorted-merge

STM: no repeats-merge

STM: strict-sorted

ABS: priority-select(f;g;as)

STM: priority-select wf

STM: priority-select-property

STM: priority-select-inr

STM: not-isl-priority-select

STM: priority-select-tt

STM: priority-select-ff

STM: fun exp add sq

STM: all-but-one

STM: no repeats member

ABS: imax-list(L)

STM: imax-list wf

STM: imax-list-ub

STM: imax-list-lb

STM: maximal-in-list

STM: member-le-max

STM: l member subtype

STM: l member subtype2

STM: l all-nil

STM: l all iff

STM: l all subtype

ABS: l_interval(l;j;i)

STM: l interval wf

STM: length l interval

STM: select l interval

STM: hd l interval

STM: last l interval

ABS: (x,yL.P(x;y))

STM: pairwise wf

STM: pairwise-nil

STM: pairwise-singleton

STM: pairwise-cons

ABS: inv-rel(A;B;f;finv)

STM: inv-rel wf

STM: inv-rel-inject

STM: hd-filter

STM: find-hd-filter

STM: list-set-type

STM: list-set-type-property

STM: list-set-type-member

STM: list-set-type2

STM: list-equal-set

STM: l member set

STM: l member set2

STM: l member-set

STM: member-mapfilter

STM: map-wf2

STM: wellfounded-anti-reflexive

STM: no-member-sq-nil

STM: l before append iff

STM: append assoc sq

STM: append-nil

STM: nil-iff-no-member

STM: tl sublist

ABS: dectt(d)

STM: dectt wf

STM: assert-dectt

STM: inr equal

STM: inl equal

STM: inl eq inr

STM: inr eq inl

ABS: finite-type(T)

STM: finite-type wf

STM: finite-type-iff-list

STM: finite-type-bool

STM: finite-set-type

STM: finite-decidable-set

STM: finite-subtype

STM: map-map

STM: map is nil

STM: map-id

STM: length-map

STM: length-map-sq

STM: select-map

STM: pairwise-map

STM: general length nth tl

STM: nth tl nil

ABS: mu(f)

STM: mu wf

STM: mu-property

STM: mu-bound

STM: mu-bound-property

STM: mu-bound-property+

STM: mu-bound-unique

ABS: upto(n)

STM: upto wf

STM: length upto

STM: upto is nil

STM: upto decomp

STM: upto iseg

STM: select upto

STM: member upto

STM: member upto2

STM: before-upto

STM: list-eq-set-type

STM: before-map

STM: filter append sq

STM: filter map upto

STM: filter map upto2

STM: member-firstn

STM: first0

STM: firstn decomp2

STM: append firstn lastn sq

STM: last-lemma-sq

STM: last-map

STM: firstn firstn

STM: firstn last

STM: firstn append

STM: firstn length

STM: firstn all

STM: firstn map

STM: firstn upto

STM: map is append

STM: map is cons

STM: decidable-last-rel

STM: decidable-exists-iseg

STM: first-iseg

STM: iseg-transition-lemma

ABS: concat(ll)

STM: concat wf

STM: concat append

STM: concat-cons

STM: concat-nil

STM: map-concat

STM: filter-concat

STM: select concat

STM: member-concat

STM: l member decomp

STM: concat-decomp

STM: last-concat

STM: concat iseg

STM: concat map upto

STM: concat-is-nil

STM: finite-type-product

STM: finite-type-union

STM: finite-type-unit

ABS: star-append(T;P;Q)

STM: star-append wf

STM: star-append-iff

STM: finite-set-type-cases

ABS: mapl(f;l)

STM: mapl wf

STM: member-mapl

STM: pairwise-mapl

ABS: CV(F)

STM: CV wf

STM: CV property

ABS: b = accum(z,x.f(z;x),a,{xX|P(x)})

STM: accum filter rel wf

STM: accum filter rel nil

STM: concat-map-decide

STM: map-decide

STM: concat-map-map-decide

STM: void-list-equality

STM: void-list-equality2

STM: void-list-equality3

STM: equal-nil-lists

ABS: SWellFounded(R(x;y))

STM: strongwellfounded wf

STM: strongwf-implies

ABS: R^+

STM: rel plus wf

STM: rel plus trans

STM: rel plus strongwellfounded

STM: rel plus implies

STM: rel exp iff

STM: rel star iff

STM: rel-star-iff-rel-plus-or

STM: rel-rel-plus

STM: rel-star-rel-plus

STM: rel-plus-rel-star

STM: rel plus iff

STM: rel plus monotone

STM: map-upto-length

STM: filter-equals

STM: implies-filter-equal

ABS: l-ordered(T;x,y.R(x;y);L)

STM: l-ordered wf

STM: no repeats-before-equality

STM: l-ordered-no repeats

STM: l-ordered-equality

ABS: Generic{f:T|S(f)}

STM: generic wf

STM: generic-non-empty

STM: pair-coding-exists

STM: finite-sequence-coding-exists

STM: generic-countable-intersection

ABS: |a/b - p/q| < 1/m

STM: ratio-dist wf

ABS: size(k;f)

STM: bool-size wf

ABS: #{i<j|f i eq x}

STM: seq-count wf

ABS: frequency(f;x) ~ (p/q)

STM: frequency wf

ABS: derived-seq(f;s)

STM: derived-seq wf

ABS: eq_seq(eq)

STM: eq seq wf

ABS: exp(i;n)

STM: exp wf

ABS: random-seq(T;sz;eq;f)

STM: random-seq wf